﻿/************************************************************************
 * AIDE - Automata Identification Engine
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     AIDE\Oracles\NFMs\Oracle_NMAT_Ideal.cs
 * Description  :     Implementation of ideal oracle for nondeterministic Mealy machines
 * Change log   :     -Date:  Change
 * To Do        :     -Jan 2013:  Initial version
 ************************************************************************/
using System;
using System.Collections.Generic;
using AIDE.Utils;
using SMLib.Automata.Base;
using SMLib.Automata.MM;

namespace AIDE.Oracles.NFMs
{
    /// <summary>
    /// This is a ideal Oracle which realy knows the language!
    /// </summary>
    public class Oracle_NMAT_Ideal : IOracle_NMM
    {
        /// <summary>
        /// input and output alphabet
        /// </summary>
        Alphabet inpAlph, outpAlph;
        DateTime startTime;
        MealyMachine SUL;
        List<ISymbol> symbs;

        /// <summary>
        /// It is used to enumerate possible outputs [in order to decrease memory usage]
        /// </summary>
        List<bool> possibleOutputs;



        public int numberOfMQ, numberOfEQ;
        public TimeSpan EqTime = TimeSpan.Zero, OqTime = TimeSpan.Zero;

        
        /// <summary>
        /// Oracle for non-deterministic Mealy Machine
        /// </summary>
        /// <param name="SUT">the target Mealy Machine</param>
        public Oracle_NMAT_Ideal(MealyMachine SUT)
        {
            numberOfEQ = 0;
            numberOfMQ = 0;
            this.SUL = SUT;
            inpAlph = SUT.InputAlphabet;
            outpAlph = SUT.OutputAlphabet;
            possibleOutputs = new List<bool>();
            for (int i = 0; i < outpAlph.Size; i++)
                possibleOutputs.Add(false);
            symbs = outpAlph.AllSymbols();
        }


        /// <summary>
        /// Input alphabet
        /// </summary>
        public Alphabet inputAlphabet
        {
            get
            {
                return inpAlph;
            }
        }

        /// <summary>
        /// This is "Output Query" of the Oracle
        /// </summary>
        /// <param name="prefix">the prefix (sequence of input/output which uniquely determines the path)</param>
        /// <param name="suffixWord">the sufix (set of input)</param>
        /// <returns>the output tree</returns>
        public Tree<ISymbol> FindOutputTree(List<PairOfSymbols> prefixSeq, List<ISymbol> suffixWord)
        {
            numberOfMQ++;
            startTime = DateTime.Now;

            //List<PairOfSymbols> emptyPair = new List<PairOfSymbols>();
            Tree<ISymbol> mytree = new Tree<ISymbol>();
            List<Tree<ISymbol>.TreeNode> myleaves = new List<Tree<ISymbol>.TreeNode>();
            List<MealyMachine.Mealy_State> mycorrespondingNodes = new List<MealyMachine.Mealy_State>();

            MealyMachine.Mealy_State m = FindNodeByPath(prefixSeq);

            mycorrespondingNodes.Add(m);
            myleaves.Add(mytree.Root);

            //* for every input in the suffix
            for (int i = 0; i < suffixWord.Count; i++)
            {
                int leavesCount = myleaves.Count;

                //* For every node in the set of leaves
                for (int j = 0; j < leavesCount; j++)
                {
                    //* leaf to be processed
                    Tree<ISymbol>.TreeNode myleaf = myleaves[0];
                    myleaves.RemoveAt(0);

                    //* corresponding node
                    MealyMachine.Mealy_State cn = mycorrespondingNodes[0];
                    mycorrespondingNodes.RemoveAt(0);

                    //* For all possible output resulting as the input
                    for (int k = 0; k < cn.Transitions.Count; k++)//(string p in po)
                    {
                        //* find a new next node (with input label=suffix[i])
                        if (((MealyMachine.Mealy_Transition)cn.Transitions[k]).inLabel.Equals(suffixWord[i]))
                        {
                            Tree<ISymbol>.TreeNode child = myleaf.AddChild(((MealyMachine.Mealy_Transition)cn.Transitions[k]).outLabel);
                            myleaves.Add(child);

                            mycorrespondingNodes.Add((MealyMachine.Mealy_State)((MealyMachine.Mealy_Transition)cn.Transitions[k]).Destination);
                        }
                    }
                }
            }
            //* Measure time
            OqTime += (DateTime.Now - startTime);
            //* return the generated tree
            return mytree;
        }


        /// <summary>
        /// 
        /// </summary>
        /// <param name="currentNode"></param>
        /// <param name="step"></param>
        /// <param name="output"></param>
        /// <returns></returns>
        MealyMachine.Mealy_State nextStep(MealyMachine.Mealy_State currentNode, ISymbol step, ISymbol output)
        {
            foreach (MealyMachine.Mealy_Transition t in currentNode.Transitions)
            {
                if (t.inLabel.Equals(step) && t.outLabel.Equals(output))
                {
                    return (MealyMachine.Mealy_State)t.Destination;
                }
            }
            return null;
        }


        MealyMachine.Mealy_State FindNodeByPath(List<PairOfSymbols> path, MealyMachine.Mealy_State initialNode = null)
        {
            MealyMachine.Mealy_State currentNode;
            if (initialNode == null)
                currentNode = (MealyMachine.Mealy_State)SUL.InitialState;
            else
                currentNode = initialNode;

            for (int i = 0; i < path.Count; i++)
            {
                currentNode = nextStep(currentNode, path[i].Input, path[i].Output);

                if (currentNode == null)
                    throw new Exception("Error: The next step is not possible!");
            }
            return currentNode;
        }



        /// <summary>
        /// [CAUSION]: you should make a backup from the return value ASAP!
        /// </summary>
        /// <param name="input"></param>
        /// <param name="output"></param>
        /// <returns></returns>
        List<bool> listOfPossibleOutput(List<PairOfSymbols> io, ISymbol lastOP, MealyMachine.Mealy_State initialNode = null)
        {
            //* To optimize:
            //* We can use the list of transition instead of wasting memory again!
            //* -> We have to increase the computation!
            //* Better way found! We should use a constant list of bools which shows which of outputs are used!
            //* -> Some of computation will even decrease
            //* TODO: We should make it private AND use output tree?


            startTime = DateTime.Now;

            for (int i = 0; i < possibleOutputs.Count; i++)
                possibleOutputs[i] = false;

            MealyMachine.Mealy_State currentNode = FindNodeByPath(io, initialNode);

            foreach (MealyMachine.Mealy_Transition t in currentNode.Transitions)
            {
                if (t.inLabel.Equals(lastOP))
                {
                    for (int i = 0; i < outpAlph.Size; i++)
                        if (symbs[i].Equals(t.outLabel))
                        {
                            possibleOutputs[i] = true;
                            break;
                        }
                }
            }

            //* Measure time
            OqTime += (DateTime.Now - startTime);

            return possibleOutputs;
        }

        /// <summary>
        /// Two corresponding nodes (of two Mealy Machine), AND the word we have seen to this state.
        /// We don'anotherRow require to also store the output (because with input, we can determine output!)
        /// 
        /// ** It is used in Hopcroft-Karp Algorithm (function EquivalenceQ, bellow) to compare two DFAs.
        /// </summary>
        class CorrespondingNodes
        {
            public CorrespondingNodes(MealyMachine.Mealy_State k, MealyMachine.Mealy_State v)
            {
                Key = k;
                Value = v;
                path = new List<PairOfSymbols>();
            }

            public CorrespondingNodes(MealyMachine.Mealy_State k, MealyMachine.Mealy_State v,
                List<PairOfSymbols> prevPath, PairOfSymbols nxt_io_step)
            {
                Key = k;
                Value = v;
                path = new List<PairOfSymbols>();
                foreach (PairOfSymbols ps in prevPath)
                    path.Add(ps);
                path.Add(nxt_io_step);
            }

            public MealyMachine.Mealy_State Key;
            public MealyMachine.Mealy_State Value;
            public List<PairOfSymbols> path;
        }


        /// <summary>
        /// See if to DFA are equal myOracle NEG. If they are NEG equal, find a counterexample to show the difference
        /// Based on Hopcroft-Karp Algorithm [A linear algorithm for testing equivalence of finite automata]
        /// </summary>
        /// <param name="conjucture"></param>
        /// <returns>
        /// if null, the models are the same.
        /// if NEG, it is a counterexample which shows the models are NEG the same
        /// </returns>
        public List<PairOfSymbols> EquivalenceQ(MealyMachine conjucture)
        {
            numberOfEQ++;
            //* Measure time
            startTime = DateTime.Now;

            //System.Diagnostics.Process currentProcess = System.Diagnostics.Process.GetCurrentProcess();
            //long totalBytesOfMemoryUsed = currentProcess.WorkingSet64;


            Stack<CorrespondingNodes> st = new Stack<CorrespondingNodes>();
            List<ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols>>>
                allSets = new List<ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols>>>();

            //* For every state q in Q1 union Q2 , MakeSet(q)
            foreach (MealyMachine.Mealy_State n in SUL.GetStates())
            {
                ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols>> equivalents =
                    new ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols>>();
                equivalents.Add(n);
                allSets.Add(equivalents);
                equivalents.value = n.ListOfAllInputOutputs();
            }

            foreach (MealyMachine.Mealy_State n in conjucture.GetStates())
            {
                ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols>> equivalents =
                    new ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols>>();
                equivalents.Add(n);
                allSets.Add(equivalents);
                equivalents.value = n.ListOfAllInputOutputs();
            }

            //* Union(s1,s2) 
            ValuedList<MealyMachine.Mealy_State, List<PairOfSymbols>> s1, s2;
            s1 = allSets[0];
            s2 = allSets[SUL.Size];
            s1.Union(s2);
            allSets.RemoveAt(SUL.Size);

            //* Push (s1,s2) on the stack
            st.Push(new CorrespondingNodes((MealyMachine.Mealy_State)SUL[0], (MealyMachine.Mealy_State)conjucture[0]));

            List<bool> possibleOutputs1 = new List<bool>();
            for (int i = 0; i < outpAlph.Size; i++)
                possibleOutputs1.Add(false);

            //* While S is non-empty
            while (st.Count != 0)
            {
                //* Pop pair (q1; q2) from Stack
                CorrespondingNodes c = st.Pop();
                List<PairOfSymbols> curentWord = c.path;

                //* For each a in Sigma 
                foreach (ISymbol a in inpAlph.AllSymbols())
                {
                    listOfPossibleOutput(curentWord, a, (MealyMachine.Mealy_State)SUL[0]);
                    //* Make a copy!
                    for (int k = 0; k < outpAlph.Size; k++)
                        possibleOutputs1[k] = possibleOutputs[k];

                    listOfPossibleOutput(curentWord, a, (MealyMachine.Mealy_State)conjucture[0]);

                    //* if the set of outputs are different, counterexample found!
                    for (int k = 0; k < outpAlph.Size; k++)
                    {
                        if (possibleOutputs1[k] != possibleOutputs[k])
                        {
                            curentWord.Add(new PairOfSymbols(a, symbs[k]));

                            //* Measure time
                            EqTime += (DateTime.Now - startTime);
                            //Console.WriteLine("Memory used for Eq Query:" + ((int)(currentProcess.WorkingSet64 - totalBytesOfMemoryUsed)));

                            return curentWord;
                        }
                    }

                    //if (po1.Count > po2.Count)
                    //    foreach (string po in po1)
                    //    {
                    //        if (!po2.Contains(po))
                    //        {
                    //            curentWord.Add(new PairOfSymbols(a.ToString(), po));
                    //            return curentWord;
                    //        }
                    //    }
                    //else
                    //    foreach (string po in po2)
                    //    {
                    //        if (!po1.Contains(po))
                    //        {
                    //            curentWord.Add(new PairOfSymbols(a.ToString(), po));
                    //            return curentWord;
                    //        }
                    //    }


                    //* for each possible output
                    for (int k = 0; k < outpAlph.Size; k++)
                    {
                        //if (!po2.Contains(po))
                        //{
                        //    /// found counterexample
                        //    curentWord.Add(new PairOfSymbols(a.ToString(), po));
                        //    return curentWord;
                        //}

                        //po2.Remove(po);

                        if (!possibleOutputs[k])
                            continue;
                        ISymbol po = symbs[k];

                        MealyMachine.Mealy_State nextA = nextStep(c.Key, a, po);
                        MealyMachine.Mealy_State nextB = nextStep(c.Value, a, po);

                        int setOfA = -1, setOfB = -1;
                        for (int i = 0; i < allSets.Count; i++)
                        {
                            if (allSets[i].Contains(nextA))
                                setOfA = i;

                            if (allSets[i].Contains(nextB))
                                setOfB = i;

                            if (setOfA > -1 && setOfB > -1) break;
                        }

                        //* if r1<>r2
                        if (setOfA != setOfB)
                        {
                            //* if outgoings of two sets are different, counterexample found!
                            //* First case: might happen for incomplete/nondeterministic mealy machine
                            if (allSets[setOfA].value.Count > allSets[setOfA].value.Count)
                            {
                                foreach (PairOfSymbols ps in allSets[setOfA].value)
                                {
                                    //* Counterexample found!
                                    if (!allSets[setOfB].value.Contains(ps))
                                    {
                                        //Word counterExample = new Word(curentWord);
                                        curentWord.Add(new PairOfSymbols(a, po));
                                        curentWord.Add(ps);
                                        //* Measure time
                                        EqTime += (DateTime.Now - startTime);
                                        //Console.WriteLine("Memory used for Eq Query:" + (currentProcess.WorkingSet64 - totalBytesOfMemoryUsed));

                                        return curentWord;
                                    }
                                }
                            }
                            else //* <=
                            {
                                foreach (PairOfSymbols ps in allSets[setOfB].value)
                                {
                                    //* Counterexample found!
                                    if (!allSets[setOfA].value.Contains(ps))
                                    {
                                        curentWord.Add(new PairOfSymbols(a, po));
                                        curentWord.Add(ps);

                                        //* Measure time
                                        EqTime += (DateTime.Now - startTime);
                                        //Console.WriteLine("Memory used for Eq Query:" +
                                        //    ((int)(currentProcess.WorkingSet64 - totalBytesOfMemoryUsed)).ToString());

                                        return curentWord;
                                    }
                                }
                            }


                            allSets[setOfA].Union(allSets[setOfB]);

                            allSets.RemoveAt(setOfB);
                            CorrespondingNodes ns = new CorrespondingNodes(nextA, nextB);
                            ns.path = new List<PairOfSymbols>(curentWord);
                            ns.path.Add(new PairOfSymbols(a, po));
                            st.Push(ns);
                        }
                    }
                }
            }

            EqTime += (DateTime.Now - startTime);
            //Console.WriteLine("Memory used for Eq Query:" + (currentProcess.WorkingSet64 - totalBytesOfMemoryUsed));

            //* Counterexample not found!
            return null;
        }

    }
}
